\section{Preliminaries}

\subsection{Basics}
\begin{lemma}[Update Semantics Basics]
  For $\rho \in \Phi \cup \{\bot\}$
  \begin{itemize}
    \item $\alpha[\rho] \sleq \alpha$
    \item  $\alpha \sleq \beta [\rho] \Longrightarrow \alpha = \alpha[\rho]$
    \item $\alpha \sleq \beta \Longrightarrow \alpha[\rho] \sleq \beta[\rho]$
    \item $\alpha = \beta \Longrightarrow \alpha[\rho] = \beta[\rho]$
    \item $\alpha [\rho][\rho] = \alpha [\rho]$
    \item $(\alpha \sqcap \beta)[\rho] = \alpha[\rho] \wedge \beta[\rho]$
  \end{itemize}
\end{lemma}
\begin{proof} ~\\ % ugly, need to find an other way.
  \begin{itemize}
    \item $\alpha[\rho] \sleq \alpha$
    \item $\alpha \sleq \beta [\rho] \Longrightarrow \alpha = \alpha[\rho]$
    \item $\alpha \sleq \beta \Longrightarrow \alpha[\rho] \sleq \beta[\rho]$
    \item $\alpha = \beta \Longrightarrow \alpha[\rho] = \beta[\rho]$
  \end{itemize}

  \begin{center}
    \ldots these facts follow directly from the definitions for update
    semantics\ldots
  \end{center}

  \begin{itemize}
  \item $\alpha [\rho][\rho] = \alpha [\rho]$: Since $\alpha [\rho] \sleq
    \alpha[\rho]$, then by the above we have $\alpha [\rho] = \alpha[\rho]
    [\rho]$
  \item $(\alpha \sqcap \beta)[\rho] = \alpha[\rho] \sqcap \beta[\rho]$:
    Observe that
    \begin{align*}
      \alpha \sqcap \beta & \sleq \alpha \\ 
      \alpha \sqcap \beta & \sleq \beta 
    \end{align*}
    \ldots whence \ldots 
    \begin{align*}
      (\alpha \sqcap \beta)[\rho] & \sleq \alpha[\rho] \\ 
      (\alpha \sqcap \beta)[\rho] & \sleq \beta[\rho]
    \end{align*}
    \ldots therefore \ldots
    \begin{align}
      (\alpha \sqcap \beta)[\rho] & \sleq \alpha[\rho] \sqcap
      \beta[\rho] \label{basiceq1}
    \end{align}
    On the other hand, we have:
    \begin{align*} 
      \alpha[\rho] \sleq \alpha \\
      \beta[\rho] \sleq \beta
    \end{align*}
    \ldots thus \ldots 
    \begin{align*} 
      \alpha[\rho] \sqcap \beta[\rho] & \sleq \alpha \sqcap \beta
    \end{align*}
    \ldots moreover \ldots
    \begin{align} 
      (\alpha[\rho] \sqcap \beta[\rho])[\rho] & \sleq (\alpha \sqcap
      \beta)[\rho] \label{basiceq2}
    \end{align}
    However, we know that
    \[ \alpha[\rho] \sqcap \beta[\rho] \sleq \alpha[\rho] \]
    \ldots which means \ldots
    \begin{align} 
      \alpha[\rho] \sqcap \beta[\rho] & = (\alpha[\rho] \sqcap
      \beta[\rho])[\rho] \label{basiceq3}
    \end{align}
    And with \eqref{basiceq1}, \eqref{basiceq2}, and \eqref{basiceq3} we have
    enough to establish that indeed, $(\alpha\sqcap \beta)[\rho] = \alpha[\rho]
    \sqcap \beta[\rho]$
  \end{itemize}
\end{proof}


\subsection{$\Box$-Reduction}
As a warm up, we note the following, essentially trivial fact about
\emph{$\Box$}. Despite its simplicity, however, it is a \emph{reduction} of
sorts. We shall need to appeal to this fact repeatedly in the completeness
theorem\ldots

\begin{lemma}[$\Box$-Reduction]
  \[ \alpha [\Box \phi] = \alpha \iff \alpha [\phi]= \alpha\]
\end{lemma}
\begin{proof}
  This follows trivially by the definition of $\alpha [\Box \phi]$\ldots
\end{proof}

\subsection{General Reflection}
Recall that the first property of the Veltman's abstract update semantics on
Boolean lattices was \emph{reflection} --  this property generalizes to all of
the formulas we shall be concerned with:
\begin{lemma}[General Reflection]
  For all $\phi \in \mathcal{L}_0 \cup \mathcal{L}_\Box \cup
  \mathcal{L}_\gillies$, we have:
  \[ \alpha [\phi] \sleq \alpha \]
\end{lemma}
\begin{proof}
  The proof proceeds first by induction on complexity of $\phi$ in
  $\mathcal{L}_0$, and then two further inductive cases for $\mathcal{L}_\Box$
  and $\mathcal{L}_\gillies$.

  As a general strategy, it shall always suffice to show that $\alpha[\phi] =
  \alpha \wedge \alpha[\phi]$

  \begin{itemize}
    \item $\rho \in \Phi \cup \{\bot\}$: This follows directly from fact that
      $\alpha[p] = \alpha\ll p\rr$ and $\ll p \rr$ is reflexive by postulate,
      and the fact that $\alpha[\bot] = \mathbf{0}$ and $\mathbf{0} \sleq
      \beta$ for all $\beta$
    \item $\neg \phi$:
      \begin{center}
        \includegraphics[]{proofs/proof2-crop.pdf}
      \end{center}
    \item $\phi \wedge \psi$:
      \begin{center}
        \includegraphics[]{proofs/proof1-crop.pdf}
      \end{center}
    \item $\Box \phi$ and $\phi \gillies \psi$:  We know that either
      $\alpha[\Box \phi] = \alpha$ or $\alpha[\Box \phi] = \mathbf{0}$,
      and likewise for $\gillies$.  Hence we know in either case that
      $\alpha[\Box \phi] \sleq \alpha$ and similarly $\alpha[\phi \gillies
      \psi ] \sleq \alpha$
  \end{itemize}
\end{proof}

\subsection{$\wedge$-Exportation}
The following lemma establishes a key link between $\wedge$ and repeated
update:
\begin{lemma}[$\wedge$-Exportation]
  For all $\{\phi,\psi\} \subseteq \mathcal{L}_0$ we have:
  \[ \alpha [\phi\wedge\psi] = \alpha [\phi][\psi] \]
\end{lemma}
\begin{proof}
  The proof proceeds by \emph{induction on $\psi$}
  \begin{itemize}
    \item $\rho \in \Phi \cup \{ \bot \}$:  First observe that $\alpha [\phi
      \wedge \rho] = \alpha [\phi] \wedge \alpha [\rho]$, and since $\alpha
      [\phi] \wedge \alpha [\rho] \sqsubseteq \alpha [\rho]$ we have that
      $\alpha [\phi \wedge \rho] \sqsubseteq \alpha [\rho]$.  But then it
      follows from the basics of update semantics that:
      \begin{center}
        \includegraphics[]{proofs/proof3-crop.pdf}
      \end{center}
      On the other hand we have from the General Reflection Lemma that $\alpha
      [\phi] = \alpha [\phi] \sqcap \alpha$, hence by the basics of update
      semantics we have:
      \begin{center}
        \includegraphics[]{proofs/proof4-crop.pdf}
      \end{center}
      Taken together, we have then that $\alpha[\phi \wedge \rho] =
      \alpha[\phi][\rho]$.
    \item $\neg \psi$: Assume we have shown the result for $\psi$.  Observe
      the following:
      \begin{center}
        \includegraphics[]{proofs/proof5-crop.pdf}
      \end{center}
    \item $\psi \wedge \chi$:  Assume the result has been shown for $\psi$ and
      $\chi$. Then we have the following:
      \begin{center}
        \includegraphics[]{proofs/proof6-crop.pdf}
      \end{center}
  \end{itemize}
  This final inductive step completes the proof.
\end{proof}

\subsection{Gillies' Equivalence}
Let $\phi \to \psi$ abbreviate $ \neg (\phi \wedge \neg \psi)$.  In
\cite{gillies_epistemic_2004}, the following is offered as Prop. 4.2(b)
\begin{lemma}[Gillies' Equivalence]
  For all $\{\phi,\psi\} \subseteq \mathcal{L}_0$ we have:
  \[ \alpha [\phi \gillies \psi] = \alpha [\Box(\phi \to \psi)] \]
\end{lemma}

\ldots the above lemma serves to reduce the semantics of Gillies' conditional
to those of $\Box$, although it is of a different character than the
$\Box$-reduction lemma. 

\begin{proof}
  First observe by $\Box$-reduction that we have the following:
  \begin{center}
    \includegraphics[]{proofs/proof7-crop.pdf}
  \end{center}
  Thus we know that if $\alpha [\Box(\phi \rightarrow \psi)] = \alpha$ then
  $\alpha [\phi \gillies \psi] = \alpha$, so then $\alpha [\Box(\phi
  \rightarrow \psi)] = \alpha [\phi \gillies \psi]$.
 
  On the other hand if $\alpha [\Box(\phi \rightarrow \psi)] \neq \alpha$ then
  $\alpha [\Box(\phi \rightarrow \psi)] = \mathbf{0}$ and moreover $\alpha
  [\phi \gillies \psi] \neq \alpha$, whence $\alpha [\phi \gillies \psi] =
  \mathbf{0}$, hence $\alpha [\Box(\phi \rightarrow \psi)] = \alpha [\phi
  \gillies \psi]$. So no matter what, we have the result.
\end{proof}

\subsection{$\gillies$-Reduction}
  \begin{lemma}[$\gillies$-Reduction]
    For $\{\varphi, \psi\} \in \mathcal{L}_0$:
    \[\alpha[\varphi \gillies \psi] = \alpha \iff \alpha[\varphi \to \psi]
    = \alpha\]
  \end{lemma}
  \begin{proof}
    This follows immediately from the Gillies' equivalence lemma and the
    $\Box$-reduction lemma.
  \end{proof}
